COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	∂28-FEB-75  1447		ESS,JMC
C00021 ENDMK
C⊗;
∂28-FEB-75  1447		ESS,JMC
 That is jmc.bio[cur,jmc].
 CC: paw

∂28-FEB-75  0521		ESS,JMC
 Yes, I can come to your committee meeting, but remind me.
 CC: ajt

∂28-FEB-75  0517		ESS,JMC
 I will be unable to come to the image understanding meeting next week, but
 I would like Tom Binford and Lynn Quam to go instead.  I have long been
 committed to a Sigma Xi lecture that conflicts, and I am going to be on
 sabbatical in Japan during the Spring quarter.  I hope that is ok.
 				John Mc
 xx
 John McCarthy
 CC: carlstrom%ISI

∂28-FEB-75  0511		ESS,JMC
 The class is in 111 Polya.
 CC: dcl

∂27-FEB-75  0010		ESS,JMC
 You forgot you had agreed to lecture in my class Tuesday.  How about lecturing
 March 11 and 13 when I have to be away?
 CC: dcl

∂25-FEB-75  0231		ESS,JMC
 I am still unhappy about the insufficient computer science content of
 the NEWS75[CUR,JMC] proposal.  However, we are in a big hurry, so please
 look again at the section entitled COMPUTER SCIENCE RESEARCH and make
 suggestions for improvement.
 CC: jh;me

∂25-FEB-75  0138		ESS,JMC
 Please order for me "Design of Man-Computer Dialogues" by Martin,Prentice-Hall.
 CC: PAW

∂24-FEB-75  1357		ESS,JMC
 Joe Goguin for ai diinner.
 CC: paw

∂24-FEB-75  1316		ESS,JMC
 Ron Kaplan makes reservation for AI dinner.
 CC: paw

∂24-FEB-75  0411		ESS,JMC
 An additional issue: Your comments on our proposal said that if we want outside
 TENEX time, we should expect to pay for it out of our budget.  Cordell wants
 a lot of it until the KL-10 is available and our system allows INTERLISP which
 he likes.  At present, he is cadging night time mostly from SRI, I think.
 At present many ARPA TENEX sites are hardly used at night.  Should we try to
 make our own deal or will ARPA help us determine what the price will be.  I
 don't now know how much I would be willing to budget, but I know I won't buy
 him a day shift PDP-10.  Is there someone else in IPT to talk to about this?
 CC: licklider%ISI

∂24-FEB-75  0343		ESS,JMC
 How do you think the following would work?  A mode of output in which the
 user program gives the system a character at a time, but the system can delay
 putting it on the user's screen until either a buffer is full or the user
 gives a display-it-now uuo.  The idea is that the user doesn't have to keep
 a buffer, and πhe system has to keep one anyway.  This would be good for
 generated rather than constant output from LISP and other programs.
 Consider it both in the context of the present system and a new one.
 CC: reg

∂23-FEB-75  0004		ESS,JMC
 Fixed.
 CC: JFR

∂22-FEB-75  2316		ESS,JMC
 CALL KAI WANG!!!!!
 CC: WD

∂22-FEB-75  1951		ESS,JMC
 Patte came in and made the first batch of changes.  I have started to
 think about changes and have decided to have separate sections on
 computer science research and behavioral research.  news75.mod[cur,jmc]
 is a start on the computer science research section.
 CC: me

∂22-FEB-75  1723		ESS,JMC
 The proposal is news75.pro[cur,jmc].
 CC: me

∂21-FEB-75  1820		ESS,JMC
 It looks like I have to go to Houston on Tuesday and be gone Wednesday,
 so I will have to reschedule.
 CC: bpm

∂21-FEB-75  1818		ESS,JMC
 Well, I thought it was supposed to be last week, but anyway I didn't do
 anything, and I guess I had better come back to the Lab and work after
 dinner, so let me postpone it.
 CC: boyer%SRI-AI

∂20-FEB-75  1855		ESS,JMC
 Your comments on our proposal are much appreciated and are giving us
 furiously to think.  I will have a message with a preliminary plan
 for meeting your requirements shortly and we will have a new draft
 in a couple weeks.  One substantive remark only because it may affect
 the second part of your remarks (if your energy persists).  While
 the KL-10 constitutes a major re-equipment, the cost to ARPA in the
 budget for this is rather small.  We believe that our plan is the
 most economical form of re-equipment.
 CC: licklider%ISI

∂20-FEB-75  1812		ESS,JMC
 brooks
 CC: Newell%CMU-10A

∂20-FEB-75  1742		ESS,JMC
 moran
 farley
 newell-control structures
 newell-stimulus encoding
 psnlst
 
 In general, examples of productions.
 CC: newell%CMU-10A

∂20-FEB-75  1633		ESS,JMC
 Send Floyd copy of Licklider comments that is on your desk.
 CC: paw

∂18-FEB-75  2253		ESS,JMC
 Please move meeting tomorrow because of Newell lecture at 3:30.
 CC: les

∂16-FEB-75  2355		ESS,JMC
 There is an error in VERIFY.TXT[EXP,TJW]; namely  9th line from bottom page 1 should be
   IF ↑CLOCK∧(S0∨S1) THEN Q[I] ← etc..
 As you have it, the register would be cleared when both S0 and S1 were low.  I am
 doubtful whether your Algol sufficiently describes the circuit to permit the
 verification of larger circuits of which it is a part.  In particular, it doesn't
 express the timing relationships that have to hold in order to get well defined
 results, e.g. the fact that S0 and S1 can change only when CLOCK is high.  I also
 have a somewhat vaguer worry that it doesn't say when the Algol statement is
 executed.  Apparently the clear can occur at any time and the other part only
 when the clock rises, and while this is hinted at by your Algol, I am not sure
 it permits the incorporation of this program into a larger Algol pr;gram
 without ambiguity.  Nevertheless, I agree with the approach.
 CC: TJW

∂16-FEB-75  1658		ESS,JMC
 I wonder if the program that receives the news could do an occasional garbage
 detection, and when it detects garbage complain to TED and TAG.
 CC: me

∂16-FEB-75  0325		ESS,JMC
 I have read your note on blobs.  Your notion of what can be done in predicate
 calculus is too limited.  Your argument is correct if the functions in the program
 are taken as functions in the logic and if we don't use axiom schemata.  Then,
 as I remarked in class in connection with Manna's method (after you gave
 me the note), a program can be shown to terminate only if it terminates in
 a number of steps independent of the parameters.  Your argument is a similar
 application of Henkin's theorem.  However, if we admit a suitable axiom schema,
 such things can be proved.  In your case the axiom schema would be
 (∀x.¬p(x)⊃Q(x))∧(∀x.p(x)∧Q(x)⊃Q(f(x))) ⊃ ∀x.Q(x).  In your trivial case, assuming
 the axiom schema is very close to assuming what fs to be proved, but
 it can also prove lots of other things about functions defined by the
 same basic recursion scheme involving  p  and  f.  Note: what I just said isn't
 quite right, because you want to allow for the fact that the recursion
 doesn't always terminate, in which case you need another predicate that
 will suitably relativize the formulas to the cases in which they do
 terminate.
 
 	However, as we shall see, one can do much better than that by making
 the functions defined recursively individuals in the logic rather than
 functions.  It is conceptually simplest to regard them as subsets of a
 product space, i.e. to represent them by their graphs, but this may not
 be most convenient practically.  If we do this, we can get by entirely with
 axioms and need know schemas even though this is again not necessarily the
 most convenient way to do it.  (The most convenient set theory is the
 Zermelo-Frankel which has an axiom schema, but the Godel-Bernays set theory
 which has no schemata is just as powerful as is shown in Cohen's book.)
 
 	Many of these matters will be treated in class, but I will be glad
 to tell you about them separately if you like.  Your proof is not incorrect;
 it merely shows the need for stronger formalisms than you imagined, and
 there is still a red herring involving non-standard models.
 CC: rae

∂16-FEB-75  0038		ESS,JMC
 No, but Monday would be nice.
 CC: nxl

∂16-FEB-75  0035		ESS,JMC
 What is present state of "r imsss"?
 CC: jbr

∂16-FEB-75  0032		ESS,JMC
 I have been too busy to extract any work from you on the LISP course notes.  You
 could help me by making up one complete copy of everything we have gotten out
 so far including exams and exercises.
 CC: nxl

∂16-FEB-75  0028		ESS,JMC
 I have read your chapter 7, and it seems to me that you must keep your mind
 in two completely separated compartments.  There is absolutely no suggestion
 in the chapter that you have ever heard of computers or information processing
 models - just old-fashioned philosophy.
 I have marked up the copy you gave me and will go over it with you.  I am
 shocked!!
 CC: ajt

∂15-FEB-75  2053		ESS,JMC
 I have several comments:
 
 	1. As I already mentioned, conditional expressions are ok.
 	2. More than half your existential quantifiers go away if you
 use the function LOC(P,B) for the location of piece P on board B, and
 your formulas simplify considerably.  In general, wherever there is a
 unique Y satisfying P(X,Y), it is better to use a function.  Allowing
 functions and equality is a common form of first order logic - not
 strictly predicate calculus - and FOL allows them.
 	3. You should rewrite your patterns with this extension, but,
 as I said before, not everything will be doable with patterns.  In
 particular, it doesn't seem to me that functions like occupiability
 are computed solely by pattern recognition.  It is a large part of your
 problem to determine what role patterns ought to play.
 CC: DEW

∂14-FEB-75  1910		ESS,JMC
 ACCEPT JAPANESE INVITATION.
 CC: :TASK.

∂14-FEB-75  1653		ESS,JMC
 Meeting with Tymshare 12:30 Tues,Tokaj Rest.,Menlo Park, RSVP.
 CC: FXB;CCG;TW

∂13-FEB-75  0123		ESS,JMC
 Thanks for FLAT proof.  I have started on first version and welcome second.
 We'll talk.
 CC: DBX

∂12-FEB-75  1620		ESS,JMC
 For Ed Frank:
 	Please telephone me 321-7580 in evening or 497-4430 afternoon.
 We can use a lot of help with further publicity of home terminal club.
 CC: nbs%ISIA

∂12-FEB-75  1451		ESS,JMC
 Tymshare tentatively 12:45pm Tuesday.
 CC: :CALEND.

∂12-FEB-75  1448		ESS,JMC
 lunch at Tymshare 12:45pm Tuesday.
 CC: :CALEND.TENTAT

∂12-FEB-75  1446		ESS,JMC
 baz
 CC: :FOO.;jmc

∂12-FEB-75  1444		ESS,JMC
 foo
 CC: :FOO.;jmc

∂12-FEB-75  1432		ESS,JMC
 Tentatively lunch at Tymshare 12:45pm Tuesday.
 CC: :CALEND;fxb;ccg;tw

∂11-FEB-75  1604		ESS,JMC
 Lucie Adam
 Story development editor, Fortune
 Time Life building
 Rockefeller Center
 New York 10020
 
 4pm Tuesday 25th,(212)556-3708
 Please send her a copy of the home terminal paper and
 put the meetin in CALEND.
 CC: paw

∂11-FEB-75  1022		ESS,JMC
 I received a fragment of a message from you.  Please retransmit it.
 CC: nbs%ISIA

∂11-FEB-75  1020		ESS,JMC
 Would you be willing to talk in my MTC class about the Hoare axioms and
 related matters?
 CC: dcl

∂11-FEB-75  0337		ESS,JMC
 Please make faculty club reservation for me for 12:30 today.
 CC: paw

∂11-FEB-75  0009		ESS,JMC
 It involves looking a gift horse in the mouth.
 CC: fxb

∂08-FEB-75  1535		ESS,JMC
 Schroeppel & Co. welcome.
 CC: SGK

∂07-FEB-75  1317		ESS,JMC
 SEE BURCHF.TMP[ESS,JMC]
 CC: PAW

∂05-FEB-75  0537		ESS,JMC AT TTY15   0537
 What is the current state of interest in NS?  You can reply by
 SEND JMC <carriage return> followed by the message followed by <ctrl z>.
 CC: JI

∂05-FEB-75  0106		ESS,JMC
 Find out whom I have to inform and how that Morales and Bulnes passed
 the MTC qual.
 CC: paw

∂03-FEB-75  1351		ESS,JMC
 Catch me sometime, and I'll tell you what I know.
 CC: ajt

∂03-FEB-75  0023		ESS,JMC
 Please decorate reynol.le3.
 CC: paw

∂02-FEB-75  2215		ESS,JMC
 I expect to be in Monday afternoon, but may go to energy seminar at 4:15.
 Before that would be best.
 CC: pmk

∂02-FEB-75  2215		ESS,JMC
 I expect to be in Monday afternoon but may go to energy seminar
 CC: pmk